perm filename HOMEW2.XGP[206,LSP]1 blob sn#386969 filedate 1978-10-05 generic text, type T, neo UTF8
/LMAR=0/XLINE=3/FONT#0=BAXL30[FNT,CLT]/FONT#1=BAXM30/FONT#2=BAXB30[FNT,CLT]/FONT#5=GACS25

␈↓ ↓H␈↓␈↓ ¬πSTANFORD UNIVERSITY

␈↓ ↓H␈↓CS206  ␈↓ βZCOMPUTING WITH SYMBOLIC EXPRESSIONS  ␈↓ 
SPRING 1978

␈↓ ↓H␈↓␈↓ ¬DPROBLEM SET  2
␈↓ ↓H␈↓␈↓ ¬rDue  May 16


␈↓ ↓H␈↓αGeneral comments.

␈↓ ↓H␈↓        This␈α⊂assignment␈α⊂involves␈α∂proving␈α⊂properties␈α⊂of␈α∂LISP␈α⊂functions.␈α⊂ Unless␈α⊂otherwise␈α∂noted
␈↓ ↓H␈↓your␈α∪proofs␈α∪should␈α∪be␈α∪fairly␈α∪formal.␈α∪ The␈α∪level␈α∪of␈α∪detail␈α∪should␈α∪be␈α∪approximately␈α∀that␈α∪of
␈↓ ↓H␈↓Chapter III␈αsection 7␈αof␈αthe␈αnotes.␈α For␈αeach␈αstep␈αof␈αyour␈αproof,␈αmake␈αsure␈αthat␈αyou␈αlist␈αall␈αof␈αthe
␈↓ ↓H␈↓facts␈α
(axioms,␈αearlier␈α
steps␈α
or␈αpreviously␈α
proved␈α
properties)␈αthat␈α
are␈α
necessary␈αto␈α
make␈α
that␈αstep.
␈↓ ↓H␈↓You may use any facts already proved in the notes or in class.


␈↓ ↓H␈↓αAssignment.

␈↓ ↓H␈↓1. Chapter III.  Exercise 1. ii-v.

␈↓ ↓H␈↓2. Chapter III.  Exercise 2.

␈↓ ↓H␈↓3.␈α
EXTRA␈α(for␈α
practice␈α
with␈αextended␈α
truth␈αvalues,␈α
not␈α
required).␈α Let␈α
␈↓↓andlist␈↓␈αbe␈α
as␈α
defined␈αin
␈↓ ↓H␈↓␈↓ α(Chapter I and assume ␈↓↓p␈↓ is a suitably well-behaved predicate.  Prove the following:

␈↓ ↓H␈↓        3.1. ␈↓↓∀u v: [andlis[u*v, p] = andlis[u, p] ∧ andlis[v, p]]␈↓

␈↓ ↓H␈↓        3.2. ␈↓↓∀u: [andlis[reverse u, p] = andlis[u, p]]␈↓

␈↓ ↓H␈↓Hint:␈αdefine␈α␈↓↓aandlis,␈↓␈αwhich␈αreturns␈αan␈αextended␈αtruth␈αvalue␈αcorresponding␈αto␈αthe␈αtruth␈αvalue␈αof
␈↓ ↓H␈↓␈↓ α(␈↓↓andlis␈↓␈α⊃on␈α⊃corresponding␈α⊃arguments.␈α⊃ Show␈α⊃that␈α⊃␈↓↓andlis␈α⊃as␈↓␈α⊃defined␈α⊃in␈α⊃terms␈α∩of␈α⊃␈↓↓aandlis␈↓
␈↓ ↓H␈↓␈↓ α(satisfies␈αthe␈αdesired␈αequivalence.␈α Then␈αyou␈αmay␈αuse␈αthis␈αresult␈αto␈αprove␈αother␈αfacts␈αabout
␈↓ ↓H␈↓␈↓ α(␈↓↓andlis.␈↓␈α The␈α
statement␈αthat␈α
"␈↓↓p␈↓␈αis␈αsuitably␈α
well-behaved"␈αis␈α
rather␈αvague.␈α
 You␈αwill␈αneed␈α
to
␈↓ ↓H␈↓␈↓ α(make it more precise in order to make your proof clear.   State this  in your proof.
␈↓ ↓H␈↓␈↓ ∧+COMPUTER SCIENCE DEPARTMENT
␈↓ ↓H␈↓␈↓ ¬πSTANFORD UNIVERSITY

␈↓ ↓H␈↓CS206  ␈↓ βZCOMPUTING WITH SYMBOLIC EXPRESSIONS  ␈↓ 
+Spring 1978

␈↓ ↓H␈↓α␈↓ ¬
Solutions for Problem Set 2.


␈↓ ↓H␈↓αGeneral comments.

␈↓ ↓H␈↓        The␈α∞following␈α∞proofs␈α∂are␈α∞generally␈α∞informal␈α∞and␈α∂emphasize␈α∞mainly␈α∞the␈α∞details␈α∂which␈α∞are
␈↓ ↓H␈↓most␈αfrequently␈αmissed.␈α
 In␈αparticular,␈αsince␈α
the␈αaxioms␈αand␈α
theorems␈αare␈αstated␈α
in␈αterms␈αof␈α
sorted
␈↓ ↓H␈↓variables␈αit␈α
is␈αimportant␈αto␈α
understand␈αthe␈αimplications␈α
of␈αthis␈α
in␈αorder␈αnot␈α
to␈αprove␈αthings␈α
which
␈↓ ↓H␈↓are␈αin␈αfact␈αfalse.␈α Thus␈αcare␈αhas␈αbeen␈αtaken␈α to␈αpoint␈αout␈αwhere␈αit␈αis␈αthat␈αterms␈αhave␈αto␈αbe␈αshown
␈↓ ↓H␈↓to␈α∪be␈α∪of␈α∪a␈α∪given␈α∩sort␈α∪in␈α∪order␈α∪that␈α∪the␈α∩axioms,␈α∪definitions,␈α∪and␈α∪theorems␈α∪can␈α∪be␈α∩applied.
␈↓ ↓H␈↓Problem 3␈αis␈αworked␈α
out␈αin␈αsome␈α
detail␈αin␈αorder␈αto␈α
provide␈αan␈αadditional␈α
example␈αof␈αthe␈α
use␈αof
␈↓ ↓H␈↓representing␈α⊂functions␈α∂and␈α⊂extended␈α⊂truthvalues␈α∂to␈α⊂prove␈α∂statements␈α⊂about␈α⊂recursively␈α∂defined
␈↓ ↓H␈↓predicates.
␈↓ ↓H␈↓        The␈α∞proofs␈α
will␈α∞be␈α
fairly␈α∞brief␈α
in␈α∞other␈α
respects␈α∞and␈α
in␈α∞particular␈α
the␈α∞basic␈α∞LISP␈α
axioms␈↓ ↓H␈↓␈↓ εH␈↓ 91
␈↓ ↓H␈↓will␈αoften␈α
used␈αwithout␈α
comment.␈α For␈α
example,␈αwe␈α
will␈αgenerally␈α
use␈αthe␈α
fact␈αthat␈α
␈↓↓issexp␈αqa␈αu␈↓␈α
and
␈↓ ↓H␈↓␈↓↓issexp␈α∞qd␈α∞u␈↓␈α∂in␈α∞the␈α∞case␈α∂that␈α∞␈↓↓¬qn␈α∞u␈↓␈α∞without␈α∂explicit␈α∞mention.␈α∞ We␈α∂will␈α∞sometimes␈α∞justify␈α∂a␈α∞step
␈↓ ↓H␈↓saying␈α∩"by␈α∩definition"␈α∩ which␈α∩means␈α∪by␈α∩using␈α∩the␈α∩functional␈α∩equation␈α∩defining␈α∪the␈α∩relevant
␈↓ ↓H␈↓function.  Some simplification (of conditional terms etc.) is usually needed to complete the step.

␈↓ ↓H␈↓        Most␈α
of␈α
the␈α
proofs␈α
are␈α
done␈α
by␈α
list␈α
or␈α
S-expression␈α
induction.␈α
 For␈α
example,␈α∞suppose␈α
you
␈↓ ↓H␈↓wish␈α
to␈α∞prove␈α
some␈α∞property␈α
␈↓↓qP[u]␈↓␈α∞for␈α
all␈α
lists␈α∞␈↓↓u.␈↓␈α
 You␈α∞first␈α
show␈α∞that␈α
qP[qNIL]␈α∞holds.␈α
 Then
␈↓ ↓H␈↓you␈αassume␈α
that␈α␈↓↓u␈↓␈α
is␈αnot␈αqNIL␈α
and␈αthat␈α
␈↓↓qP[qd␈αu]␈↓␈αholds␈α
and␈αshow␈α
that␈αunder␈α
these␈αassumptions
␈↓ ↓H␈↓␈↓↓qP[u]␈↓␈α⊃is␈α⊃true.␈α⊃ The␈α⊃fact␈α⊃that␈α⊃␈↓↓qP[u]␈↓␈α⊃holds␈α⊃for␈α⊃all␈α⊃lists␈α⊃␈↓↓u␈↓␈α⊃then␈α⊃follows␈α⊃by␈α⊃list␈α⊃induction.␈α⊂ The
␈↓ ↓H␈↓situation for S-expression induction is analogous.


␈↓ ↓H␈↓αProblem 1.

␈↓ ↓H␈↓        We will use the following facts about the operator < >:

␈↓ ↓H␈↓1.0             ␈↓↓∀x: islist <x>␈↓   and    ␈↓↓∀x u: <x> * u = x . u␈↓

␈↓ ↓H␈↓These␈αfacts␈α
are␈αa␈α
simple␈αconsequence␈α
of␈αthe␈α
definitions␈αof␈α
*,␈α<>␈α
and␈αthe␈α
LISP␈αaxioms.␈α
 We␈αwill
␈↓ ↓H␈↓also use the result of Problem 1.i which was proved in class.

␈↓ ↓H␈↓αProof of 1.ii         ␈↓↓∀u: islist reverse1 u␈↓α


␈↓ ↓H␈↓Method: list induction with   ␈↓↓qP[u] ≡ islist reverse1 u␈↓.

␈↓ ↓H␈↓Case ␈↓↓qn u␈↓:

␈↓ ↓H␈↓    ␈↓↓islist reverse1 u ≡ islist qNIL␈↓    ...by definition of ␈↓↓reverse1␈↓
␈↓ ↓H␈↓                        ≡ T   ...by the LISP axioms.

␈↓ ↓H␈↓Case  ␈↓↓¬qn u␈↓ and ␈↓↓islist reverse1 qd u␈↓

␈↓ ↓H␈↓    ␈↓↓islist reverse1 u ≡ islist [reverse1 qd u * <qa u>]␈↓   ...by definition  of ␈↓↓reverse1␈↓
␈↓ ↓H␈↓                        ≡  T   ...by induction hypothesis, ␈↓¬ISLIST-APPEND ␈↓and 1.0.


␈↓ ↓H␈↓αProof of 1.iii  ␈↓↓∀u: reverse u = reverse1 u␈↓α

␈↓ ↓H␈↓        We prove a slightly more general result, namely

␈↓ ↓H␈↓1.1             ␈↓↓∀u v: reverse1 u * v = rev[u,v]␈↓

␈↓ ↓H␈↓then taking ␈↓↓v␈↓ = qNIL the desired result follows by 1.i  and the definition of ␈↓↓reverse.␈↓

␈↓ ↓H␈↓Method: list induction with   ␈↓↓qP[u] ≡ ∀v: reverse1 u * v = rev[u,v]␈↓.

␈↓ ↓H␈↓Case  ␈↓↓qn u␈↓

␈↓ ↓H␈↓    ␈↓↓reverse1 qNIL * v = v␈↓   ...by definition of ␈↓↓reverse1␈↓ and ␈↓¬NIL-APPEND ␈↓
␈↓ ↓H␈↓                      ␈↓↓= rev[u,v]␈↓   ...by definition of ␈↓↓rev␈↓ .

␈↓ ↓H␈↓Case  ␈↓↓¬qn u␈↓ and ␈↓↓∀v: reverse1 qd u * v = rev[qd u,v]␈↓:

␈↓ ↓H␈↓    ␈↓↓reverse1 u = reverse1 qd u * <qa u>␈↓   ...by definition
␈↓ ↓H␈↓                    ␈↓↓= rev[qd u,<qa u>]␈↓   ...by induction hypothesis and ␈↓↓islist <qa u>␈↓␈↓ ↓H␈↓␈↓ εH␈↓ 92
␈↓ ↓H␈↓                    ␈↓↓= rev[u,qNIL]␈↓   ...by definition.

␈↓ ↓H␈↓        From␈α⊂here␈α⊃on␈α⊂we␈α⊂shall␈α⊃use␈α⊂␈↓↓reverse␈↓␈α⊂and␈α⊃␈↓↓reverse1␈↓␈α⊂interchangably.␈α⊂ As␈α⊃1.iv␈α⊂is␈α⊃more␈α⊂easily
␈↓ ↓H␈↓proved using 1.v, we will prove 1.v next.

␈↓ ↓H␈↓αProof of 1.v  ␈↓↓∀u v: reverse[u * v] = reverse v * reverse u␈↓α

␈↓ ↓H␈↓Method: list induction with ␈↓↓qP[u] ≡ ∀v: reverse[u * v] = reverse v * reverse u␈↓.

␈↓ ↓H␈↓Case ␈↓↓qn u␈↓:

␈↓ ↓H␈↓    ␈↓↓reverse[qNIL * v] = reverse v␈↓   ...by ␈↓¬NIL-APPEND ␈↓
␈↓ ↓H␈↓                   ␈↓↓= reverse v * qNIL␈↓   ...by 1.i
␈↓ ↓H␈↓                   ␈↓↓= reverse v * reverse qNIL␈↓   ...by definition.

␈↓ ↓H␈↓Case    ␈↓↓¬qn u␈↓ and ␈↓↓∀v: reverse[qd u * v] = reverse v * reverse qd u␈↓:

␈↓ ↓H␈↓    ␈↓↓reverse[u * v] = reverse[qd u * v] * <qa u>␈↓   ...by definition, ␈↓¬CAR/CDR-APPEND ␈↓and ␈↓↓islist u*v␈↓
␈↓ ↓H␈↓                    ␈↓↓= [reverse v * reverse qd u] * <qa u>␈↓   ...by induction hypothesis
␈↓ ↓H␈↓                    ␈↓↓= reverse v * [reverse qd u * <qa u>]␈↓   ...by ␈↓¬ASSOC-APPEND ␈↓
␈↓ ↓H␈↓                ...here we need ␈↓↓islist reverse v␈↓, ␈↓↓islist reverse qd u␈↓ and ␈↓↓islist <qa u>␈↓
␈↓ ↓H␈↓                    ␈↓↓= reverse v * reverse u␈↓   ...by definition

␈↓ ↓H␈↓αProof of 1.iv   ␈↓↓∀u: reverse reverse u = u␈↓α

␈↓ ↓H␈↓Method: list induction with    ␈↓↓qP[u] ≡ reverse reverse u = u␈↓.

␈↓ ↓H␈↓Case ␈↓↓qn u␈↓:

␈↓ ↓H␈↓    ␈↓↓reverse reverse qNIL = reverse qNIL = qNIL␈↓   ... by definition

␈↓ ↓H␈↓Case    ␈↓↓¬qn u␈↓ and ␈↓↓reverse reverse qd u = qd u␈↓:

␈↓ ↓H␈↓    ␈↓↓reverse reverse u = reverse[reverse qd u * <qa u>]␈↓   ...by definition
␈↓ ↓H␈↓                    ␈↓↓= reverse <qa u> * reverse reverse qd u␈↓   ... by 1.v
␈↓ ↓H␈↓             ...here we need ␈↓↓islist reverse qd u␈↓ and ␈↓↓islist <qa u>␈↓
␈↓ ↓H␈↓                    ␈↓↓= <qa u> * qd u␈↓   ...by induction hypothesis and computation  using ␈↓↓islist <qa u>␈↓
␈↓ ↓H␈↓                    ␈↓↓= u␈↓   ...by 1.0 and the LISP axioms


␈↓ ↓H␈↓This␈αends␈αProblem␈α1␈αas␈αassigned.␈α The␈αproof␈αof␈αthe␈αequivalence␈αof␈α␈↓↓flatten␈↓␈αand␈α␈↓↓fringe␈↓␈αas␈αoutlined
␈↓ ↓H␈↓in class is included here for completeness.

␈↓ ↓H␈↓αProof ␈↓↓∀x u: flat[x,u] = fringe x * u␈↓α

␈↓ ↓H␈↓Method: S-expression induction with   ␈↓↓qP[x] ≡ ∀u: flat[x,u] = fringe x * u␈↓.

␈↓ ↓H␈↓Case ␈↓↓qat x␈↓:

␈↓ ↓H␈↓    ␈↓↓flat[x,u] = x . u␈↓    ...by definition
␈↓ ↓H␈↓              ␈↓↓= <x> * u␈↓   ... by 1.0
␈↓ ↓H␈↓              ␈↓↓= fringe x * u␈↓  ... by definition

␈↓ ↓H␈↓Case   ␈↓↓¬qat x␈↓ and ␈↓↓∀u: flat[qd x,u] = fringe qd x * u␈↓ :
␈↓ ↓H␈↓    ␈↓↓flat[x,u] = flat[qa x,flat[qd x,u]]␈↓   ...by definition␈↓ ↓H␈↓␈↓ εH␈↓ 93
␈↓ ↓H␈↓                    ␈↓↓= flat[qa x,fringe qd x * u]␈↓   ...by induction hypothesis
␈↓ ↓H␈↓                    ␈↓↓= fringe qa x * [fringe qd x * u]␈↓   ...again by induction hypothesis
␈↓ ↓H␈↓                                            ...here we need ␈↓↓islist fringe qd x * u␈↓
␈↓ ↓H␈↓                    ␈↓↓= fringe x * u␈↓   ...by ␈↓¬ISTOT-APPEND ␈↓and definition of ␈↓↓fringe␈↓
␈↓ ↓H␈↓                           ...here we need ␈↓↓islist fringe qd x ␈↓ and ␈↓↓islist fringe qa x␈↓



␈↓ ↓H␈↓αProblem 2.

␈↓ ↓H␈↓        In␈α
proving␈α
the␈α
desired␈α
fact␈α
about␈α
␈↓↓subst,␈↓␈α
␈↓↓sublis,␈↓␈α
and␈α
@␈α
we␈α
will␈α
use␈α
a␈α
new␈α
sort␈α∞␈↓↓slist.␈↓␈α
 The
␈↓ ↓H␈↓variables␈α∀␈↓↓s,␈↓␈α∀␈↓↓s1,␈↓␈α∪␈↓↓s2,␈↓␈α∀␈↓↓s3␈↓␈α∀range␈α∀over␈α∪the␈α∀domain␈α∀characterized␈α∪by␈α∀the␈α∀predicate␈α∀␈↓↓slist.␈↓␈α∪ We
␈↓ ↓H␈↓axiomatize slists as follows:

␈↓ ↓H␈↓2.1     ␈↓↓∀X: [slist X ≡ islist X ∧ [qn X ∨ [¬qat qa X ∧ slist qd X]]]␈↓   ...X is a general variable.

␈↓ ↓H␈↓Thus ␈↓↓s␈↓ is either qNIL or a list of nonatomic elements.   We shall also use the following facts.

␈↓ ↓H␈↓2.2     ␈↓↓∀x y: [occur[x,y] ≡ [x=y] ∨ [¬qat y ∧ [occur[x, qa y] ∨ occur[x,qd y]]]]␈↓
␈↓ ↓H␈↓2.3     ␈↓↓∀x s: [qn assoc[x,s] ∨ [issexp assoc[x,s] ∧ ¬qat assoc[x,s]]]␈↓
␈↓ ↓H␈↓2.4     ␈↓↓∀s1 s2:  slist s1 * s2␈↓
␈↓ ↓H␈↓2.5     ␈↓↓∀z s1 s2: [assoc[z,s1*s2] = qif qn assoc[z,s1] qthen assoc[z,s2] qelse assoc[z,s1]]␈↓
␈↓ ↓H␈↓2.6     ␈↓↓∀x y z: issexp subst[x, y, z]␈↓
␈↓ ↓H␈↓2.7     ␈↓↓∀x,s: issexp sublis[x,s]␈↓
␈↓ ↓H␈↓2.8     ␈↓↓∀s1 s2: slist subsub[s1,s2]␈↓
␈↓ ↓H␈↓        ␈↓↓∀s1 s2:  ¬qn s1 ⊃ ¬qn subsub[s1,s2]␈↓
␈↓ ↓H␈↓        ␈↓↓∀s1 s2:  ¬qn s1 ⊃ qd subsub[s1,s2] = subsub[qd s1,s2]␈↓
␈↓ ↓H␈↓2.9     ␈↓↓∀s1 s2: slist s1@s2␈↓

␈↓ ↓H␈↓The␈αproof␈αof␈α2.2␈αis␈αoutlined␈αin␈α
the␈αtext␈αand␈α2.3␈α-␈α2.9␈αcan␈α
be␈αproved␈αby␈αstraight␈αforward␈αlist␈αor␈α
S-
␈↓ ↓H␈↓expression induction using the LISP axioms function definitions and 2.1.

␈↓ ↓H␈↓αProof of 2.i   ␈↓↓∀x y z: subst[x, y, z] = sublis[z, <x,y>]␈↓α


␈↓ ↓H␈↓Method: S-expression induction with   ␈↓↓qP[z] ≡ ∀x y: subst[x,y,z] = sublis[z,<x.y>]␈↓.

␈↓ ↓H␈↓Case ␈↓↓qat z␈↓:

␈↓ ↓H␈↓    ␈↓↓subst[x,y,z] = qif y=z qthen x qelse z␈↓    ...by definition of ␈↓↓subst␈↓
␈↓ ↓H␈↓    ␈↓↓sublis[z,<y.x>] = {assoc[z,<y.x>]}[λz1: qif qn z1 qthen z qelse qd z1]␈↓   ... by definition of ␈↓↓sublis␈↓
␈↓ ↓H␈↓                    ␈↓↓= qif y≠z qthen z qelse qd y.x␈↓    ...by computation since ␈↓↓slist <y.x>␈↓.

␈↓ ↓H␈↓Case ␈↓↓¬qat z␈↓ and ␈↓↓∀x y: [subst[x, y, qa z] = sublis[qa z, <y.x>] ∧ subst[x,y,qd z] = sublis[qd z,<y.x␈↓

␈↓ ↓H␈↓    ␈↓↓subst[x,y,z] = subst[x,y,qa z] . subst[x,y,qd z]␈↓    ...by definition of ␈↓↓subst␈↓
␈↓ ↓H␈↓                    ␈↓↓= sublis[qa z, <y.x>] . sublis[qd z,<y.x>]␈↓    ...by induction hypothesis
␈↓ ↓H␈↓                    ␈↓↓= sublis[z,<y.x>]␈↓    ...by definition of ␈↓↓sublis.␈↓


␈↓ ↓H␈↓        Before proving (ii) we prove some lemmas.  Namely

␈↓ ↓H␈↓2.10    ␈↓↓∀z s1 s2: [qn assoc[z, s1] ⊃ assoc[z, s1@s2] = assoc[z,s2]]␈↓
␈↓ ↓H␈↓2.11    ␈↓↓∀z s1 s2:  [¬qn assoc[z,s1] ⊃ ¬qn assoc[z,s1@s2] ∧ qd assoc[z,s1@s2] = sublis[qd assoc[z,s1],␈↓
␈↓ ↓H␈↓These␈αare␈αfairly␈αsimple␈αconsequences␈αof␈αthe␈αfacts␈αmentioned␈αat␈αthe␈αbeginning␈αof␈αthis␈αproblem␈α
and␈↓ ↓H␈↓␈↓ εH␈↓ 94
␈↓ ↓H␈↓the following statement:

␈↓ ↓H␈↓2.12    ␈↓↓∀z s1 s2: [qn assoc[z, s1] ≡ qn assoc[z,subsub[s1,s2]]]␈↓
␈↓ ↓H␈↓                ␈↓↓∧ [¬qn assoc[z,s1] ⊃ qd assoc[z,subsub[s1,s2] = sublis[qd assoc[z,s1],s2]]␈↓


␈↓ ↓H␈↓αProof of 2.12.

␈↓ ↓H␈↓Method:  list induction on ␈↓↓s1.␈↓

␈↓ ↓H␈↓Case ␈↓↓qn s1␈↓:

␈↓ ↓H␈↓    Both sides of the equivalence reduce to ␈↓↓qn qNIL␈↓ and the left hand side of ⊃ is F.


␈↓ ↓H␈↓Case ␈↓↓¬qn s1␈↓ and ␈↓↓∀z s2: [qn assoc[z, qd s1] ≡ qn assoc[z,subsub[qd s1,s2]]]␈↓
␈↓ ↓H␈↓                   ␈↓↓∀z s2: [¬qn assoc[z,qd s1] ⊃ qd assoc[z,subsub[qd s1,s2] = sublis[qd assoc[z,qd s1], ␈↓

␈↓ ↓H␈↓    ␈↓↓assoc[z,subsub[s1,s2]] = qif z=qaa subsub[s1,s2] qthen qa subsub[s1,s2] qelse assoc[z,subsub[qd ␈↓
␈↓ ↓H␈↓           ...by definition of ␈↓↓assoc␈↓
␈↓ ↓H␈↓           ...here we need ␈↓↓slist subsub[s1,s2]␈↓, ␈↓↓¬qn subsub[s1,s2]␈↓ and ␈↓↓qd subsub[s1,s2] = subsub[qd s1␈↓
␈↓ ↓H␈↓                ␈↓↓= qif z = qaa s1 qthen [qaa s1 . sublis[qda s1,s2]] qelse assoc[z, subsub[qd s1,s2]]␈↓
␈↓ ↓H␈↓           ...here we need in addition, 2.1, the definition of ␈↓↓subsub␈↓ and ␈↓↓issexp sublis[qda s1,s2]␈↓

␈↓ ↓H␈↓Subcase  ␈↓↓z = qaa s1 ␈↓:  the result follows from the definitions by computation.

␈↓ ↓H␈↓Subcase   ␈↓↓z ≠ qaa s1␈↓: the result follows from the induction hypothesis and definition of ␈↓↓assoc.␈↓


␈↓ ↓H␈↓αProof of 2.10

␈↓ ↓H␈↓Assume: ␈↓↓qn assoc[z,s1]␈↓

␈↓ ↓H␈↓    ␈↓↓qn assoc[z, subsub[s1,s2]]␈↓    ... by 2.12
␈↓ ↓H␈↓    ␈↓↓assoc[z,subsub[s1,s2]*s2] = assoc[z,s1@s2] = assoc[z,s2]␈↓   ...by 2.5 and definition of @.


␈↓ ↓H␈↓αProof of 2.11

␈↓ ↓H␈↓Assume: ␈↓↓¬qn assoc[z,s1]␈↓

␈↓ ↓H␈↓    ␈↓↓¬qn assoc[z,subsub[s1,s2]]␈↓    ...by 2.12
␈↓ ↓H␈↓    ␈↓↓assoc[z,s1@s2] = assoc[z,subsub[s1,s2]]␈↓    ...by 2.5 and definition of @

␈↓ ↓H␈↓The result then follows from the second part of 2.12 and ␈↓¬NOTNIL-APPEND. ␈↓


␈↓ ↓H␈↓αProof of 2.ii   ␈↓↓∀z s1 s2: sublis[z,s1@s2] = sublis[sublis[z,s1],s2]␈↓α.

␈↓ ↓H␈↓Method: S-expression induction with ␈↓↓qP[z] ≡ ∀s1 s2: sublis[z,s1@s2] = sublis[sublis[z,s1],s2]␈↓.

␈↓ ↓H␈↓Case ␈↓↓qat z␈↓:

␈↓ ↓H␈↓    ␈↓↓sublis[z,s1@s2] = {assoc[z,s1@s2]}[λz1: qif qn z1 qthen z qelse qd z1]␈↓
␈↓ ↓H␈↓    ␈↓↓sublis[z,s1] = {assoc[z,s1]}[λz1: qif qn z1 qthen z qelse qd z1]␈↓
␈↓ ↓H␈↓If ␈↓↓qn assoc[z,s1]␈↓ the result follows from 2.10 and if ␈↓↓¬qn assoc[z,s1]␈↓ the result follows from 2.11.␈↓ ↓H␈↓␈↓ εH␈↓ 95

␈↓ ↓H␈↓Case  ␈↓↓¬qat z␈↓ and ␈↓↓∀s2: [sublis[qa z, s1@s2] = sublis[sublis[qa z,s1],s2]␈↓
␈↓ ↓H␈↓                ∧ ␈↓↓∀s2: [sublis[qd z, s1@s2] = sublis[sublis[qd z,s1],s2]␈↓

␈↓ ↓H␈↓    ␈↓↓sublis[z,s1@s2] = sublis[qa z,s1@s2] . sublis[qd z,s1@s2]␈↓   ...by definition
␈↓ ↓H␈↓                    ␈↓↓= sublis[sublis[qa z,s1],s2] . sublis[sublis[qd z,s1],s2]␈↓    ...by induction
␈↓ ↓H␈↓                    ␈↓↓= sublis[sublis[z,s1],s2]␈↓   ... by definition of ␈↓↓sublis␈↓
␈↓ ↓H␈↓           ...here we need ␈↓↓issexp sublis[qa z,s1]␈↓ and ␈↓↓issexp sublis[qd z,s1]␈↓



␈↓ ↓H␈↓αProof of 2.iii ␈↓↓∀z s1 s2 s3: sublis[z, s1@[s2@s3]] = sublis[z, [s1@s2]@s3]]␈↓α

␈↓ ↓H␈↓        This is a direct consequence of 2.ii and ␈↓↓slist s1@s2␈↓ as follows:

␈↓ ↓H␈↓                ␈↓↓sublis[z, s1@[s2@s3]] = sublis[sublis[z,s1],s2@s3] ␈↓
␈↓ ↓H␈↓                                ␈↓↓= sublis[sublis[sublis[z,s1],s2],s3]␈↓
␈↓ ↓H␈↓                                ␈↓↓= sublis[sublis[z,s1@s2],s3]␈↓
␈↓ ↓H␈↓                                ␈↓↓= sublis[z, [s1@s2]@s3]␈↓


␈↓ ↓H␈↓αProof of 2.iv  ␈↓↓∀x y z: [¬occur[y,z] ⊃ subst[x,y,z] = z]␈↓α

␈↓ ↓H␈↓Method: S-expression induction with  ␈↓↓qP[z] ≡ ∀x y: [¬occur[y,z] ⊃ subst[x,y,z] = z]␈↓.

␈↓ ↓H␈↓Case ␈↓↓qat z␈↓:

␈↓ ↓H␈↓    ␈↓↓¬occur[y,z] ≡ y≠z␈↓ and ␈↓↓subst[x,y,z] = qif y = z qthen x qelse z␈↓ so qP holds.

␈↓ ↓H␈↓Case ␈↓↓¬qat z␈↓ and ␈↓↓∀x y: [¬occur[y, qa z] ⊃ subst[x,y,qa z] = qa z ∧  [¬occur[y, qd z] ⊃ subst [x,y,qd␈↓

␈↓ ↓H␈↓    ␈↓↓¬occur[y,z] ≡ y≠z ∧ ¬occur[y,qa z] ∧ ¬occur[y,qd z]␈↓
␈↓ ↓H␈↓    ␈↓↓subst[x,y,z] = subst[x,y,qa z] . subst[x,y,qd z]␈↓    ...by definition
␈↓ ↓H␈↓                 ␈↓↓= qa z . qd z␈↓   ...by induction hypothesis
␈↓ ↓H␈↓                 ␈↓↓= z␈↓

␈↓ ↓H␈↓␈↓αProof  of  2.v␈↓ ␈↓↓∀x  x1  y  y1  z:  [y ≠  y1  ∧  ¬occur[y,  x1]]  ⊃ ␈↓
␈↓ ↓H␈↓                                    ␈↓↓subst[x1,y1,subst[x,y,z]] = subst[subst[x1,y1,x],y,subst[x1,y1,z]]␈↓

␈↓ ↓H␈↓Method: S-expression induction on ␈↓↓z.␈↓

␈↓ ↓H␈↓Case ␈↓↓qat z␈↓:

␈↓ ↓H␈↓    ␈↓↓subst[x1,y1,subst[x,y,z]] = qif y=z qthen subst[x1,y1,x] qelse qif y1=z qthen x1 qelse z␈↓

␈↓ ↓H␈↓    ␈↓↓subst[subst[x1,y1,x],y,subst[x1,y1,z]] ␈↓
␈↓ ↓H␈↓                ␈↓↓= qif y1=z qthen qif y=x1 qthen subst[x1,y1,x] qelse x1␈↓
␈↓ ↓H␈↓                            ␈↓↓qelse qif y=z qthen subst[x1,y1,x] qelse z␈↓
␈↓ ↓H␈↓                ␈↓↓=qif y1=z qthen x1 qelse qif y=z qthen subst[x1,y1,x] qelse z␈↓   ...since  ␈↓↓¬occur[y,x1]␈↓

␈↓ ↓H␈↓The result now follows by a simple case analysis since ␈↓↓y=z␈↓ and ␈↓↓y1=z␈↓ can not both be true.

␈↓ ↓H␈↓Case ␈↓↓¬qat z␈↓ and ␈↓↓∀x  x1  y  y1:  [y  ≠  y1  ∧  ¬occur[y,  x1]]  ⊃␈↓
␈↓ ↓H␈↓        ␈↓↓subst[x1,y1,subst[x,y,qa z] = subst[subst[x1,y1,x],y,subst[x1,y1,qa z]]␈↓
␈↓ ↓H␈↓        ␈↓↓∧ subst[x1,y1,subst[x,y,qd z] = subst[subst[x1,y1,x],y,subst[x1,y1,qd z]]]␈↓
␈↓ ↓H␈↓    ␈↓↓subst[x1,y1,subst[x,y,z]] = subst[x1,y1,subst[x,y,qa z] . subst[x,y,qd z]]␈↓␈↓ ↓H␈↓␈↓ εH␈↓ 96
␈↓ ↓H␈↓                ␈↓↓= subst[x1,y1,subst[x,y,qa z]] . subst[x1,y1,[subst[x,y,qd z]]␈↓
␈↓ ↓H␈↓                      ...here we need ␈↓↓issexp subst[x,y,qa z]␈↓ and ␈↓↓issexp subst[x,y,qd z]␈↓
␈↓ ↓H␈↓                ␈↓↓= subst[subst[x1,y1,x],y,subst[x1,y1,qa z]] . subst[subst[x1,y1,x],y,subst[x1,y1,qd ␈↓
␈↓ ↓H␈↓                ␈↓↓= subst[subst[x1,y1,x],y,subst[x1,y1,z]]␈↓

␈↓ ↓H␈↓This completes problem 2.


␈↓ ↓H␈↓αProblem 3.

␈↓ ↓H␈↓        We wish to prove the following two statements:

␈↓ ↓H␈↓(i)     ␈↓↓∀u v: andlis[u*v,phi] ≡ andlis[u,phi] ∧ andlis[v,phi]␈↓

␈↓ ↓H␈↓(ii)    ␈↓↓∀u: andlis[u,phi] ≡ andlis[reverse u,phi]␈↓

␈↓ ↓H␈↓where␈α∂␈↓↓phi␈↓␈α∂is␈α∂a␈α∂unary␈α∂predicate.␈α∂ (The␈α∂use␈α∂of␈α∂␈↓↓p␈↓␈α∂in␈α∂the␈α∂original␈α∂porblem␈α∂statement␈α∂was␈α⊂a␈α∂poor
␈↓ ↓H␈↓choice␈α
as␈α
␈↓↓p␈↓␈α
is␈α∞designated␈α
in␈α
Chapter␈α
3␈α
as␈α∞a␈α
variable␈α
of␈α
type␈α
␈↓↓istv.)␈↓␈α∞ Note␈α
that␈α
even␈α
to␈α∞state␈α
this
␈↓ ↓H␈↓problem␈α
requires␈αan␈α
extension␈αto␈α
the␈αsyntax␈α
of␈α
our␈αlanguage␈α
in␈αorder␈α
to␈αallow␈α
functions␈αthat␈α
have
␈↓ ↓H␈↓functions␈α
as␈α
arguments.␈α
 In␈α∞the␈α
problem␈α
␈↓↓phi␈↓␈α
is␈α∞considered␈α
as␈α
a␈α
parameter.␈α∞ (Quantification␈α
over
␈↓ ↓H␈↓predicates is not allowed.)

␈↓ ↓H␈↓        The␈α
strategy␈α
for␈α
doing␈αthe␈α
proof␈α
is␈α
as␈α
follows.␈α We␈α
define␈α
a␈α
representing␈α
function␈α␈↓↓aandlis␈↓
␈↓ ↓H␈↓for␈α∩␈↓↓andlis.␈↓␈α⊃ To␈α∩do␈α⊃this␈α∩we␈α⊃need␈α∩to␈α∩know␈α⊃that␈α∩␈↓↓phi␈↓␈α⊃has␈α∩a␈α⊃representing␈α∩function␈α∩␈↓↓pphi.␈↓␈α⊃ The
␈↓ ↓H␈↓statement␈α∩that␈α∩␈↓↓phi␈↓␈α∩is␈α∪suitable␈α∩well␈α∩behaved␈α∩becomes␈α∩then␈α∪the␈α∩statement␈α∩that␈α∩␈↓↓pphi␈↓␈α∪maps␈α∩S-
␈↓ ↓H␈↓expressions into the domain ␈↓¬TV ␈↓and maps general objects into the domain ␈↓¬ETV. ␈↓ Thus

␈↓ ↓H␈↓3.1     ␈↓↓∀u: [aandlis[u,pphi] = nnull u oor [pphi qa u aand aandlis[qd u,pphi]]␈↓
␈↓ ↓H␈↓3.2     ␈↓↓∀u: isetv aandlis qd u␈↓
␈↓ ↓H␈↓3.3     ␈↓↓∀u: isetv pphi qa u␈↓
␈↓ ↓H␈↓3.4     ␈↓↓∀x: istv pphi x␈↓
␈↓ ↓H␈↓3.5     ␈↓↓∀x: [phi x ≡ pphi x=␈↓¬TT␈↓↓]␈↓
␈↓ ↓H␈↓3.6     ␈↓↓∀u: [andlis[u,phi] ≡ aandlis[u,pphi] = ␈↓¬TT␈↓↓]␈↓

␈↓ ↓H␈↓Here␈α∞␈↓↓nnull␈↓␈α
is␈α∞defined␈α∞similarly␈α
to␈α∞␈↓↓aatom␈↓␈α
and␈α∞we␈α∞assume␈α
the␈α∞analagous␈α
results␈α∞such␈α∞as␈α
␈↓¬TVNNUL,
␈↓ ↓H␈↓¬␈↓and␈α␈↓¬EQNNUL.␈α␈↓␈α3.2␈αand␈α3.3␈αare␈αneeded␈αinorder␈αto␈αbe␈αable␈αto␈αuse␈αthe␈αdefinitions␈αof␈α␈↓↓aand␈↓␈αand␈α␈↓↓oor␈↓␈αin
␈↓ ↓H␈↓the case ␈↓↓qn u␈↓. Using these axioms we prove

␈↓ ↓H␈↓3.7     ␈↓↓∀u: istv aandlis[u,pphi]␈↓

␈↓ ↓H␈↓from which we get (using ␈↓¬EQAAND ␈↓␈↓¬EQOOR ␈↓etc., and the above axioms)  that

␈↓ ↓H␈↓3.8     ␈↓↓∀u: [andlis[u,phi] ≡ qn u ∨ [phi qa u ∧ andlis[qd u,phi]]␈↓.

␈↓ ↓H␈↓This last statement is used together with list induction to prove the desired results.


␈↓ ↓H␈↓αProof of 3.7

␈↓ ↓H␈↓Method: list induction with ␈↓↓qP[u] ≡ istv aandlis[u,pphi]␈↓.
␈↓ ↓H␈↓Case ␈↓↓qn u␈↓:

␈↓ ↓H␈↓    ␈↓↓istv aandlis[u,pphi] ≡ istv ␈↓¬TT␈↓↓␈↓ ...by  definitions of ␈↓↓nnull,␈↓ ␈↓↓aand,␈↓ ␈↓↓oor,␈↓ 3.1, 3.2 and 3.3 .

␈↓ ↓H␈↓Case ␈↓↓¬qn u␈↓  and ␈↓↓istv aandlis[qd u,pphi]␈↓:
␈↓ ↓H␈↓    ␈↓↓istv aandlis[u,pphi]␈↓ follows by definition and ␈↓¬TVOOR ␈↓from␈↓ ↓H␈↓␈↓ εH␈↓ 97
␈↓ ↓H␈↓        ␈↓↓[istv nnull u]∧[istv [pphi qa u aand aandlis[qd u,pphi]]␈↓
␈↓ ↓H␈↓but we have
␈↓ ↓H␈↓    ␈↓↓istv [pphi qa u aand aandlis[qd u,pphi]␈↓   ...by induction, ␈↓¬TVAND ␈↓and 3.4
␈↓ ↓H␈↓    ␈↓↓istv [nnull u]␈↓   ..by remarks above


␈↓ ↓H␈↓αProof of 3.i.

␈↓ ↓H␈↓Method: list induction with  ␈↓↓qP[u] ≡ ∀v: [andlis[u*v,phi] ≡ andlis[u,phi] ∧ andlis[v,phi]]␈↓

␈↓ ↓H␈↓Case ␈↓↓qn u␈↓:

␈↓ ↓H␈↓    ␈↓↓andlis[u*qNIL,phi] ≡ andlis[u,phi]␈↓   ...by ␈↓¬NIL-APPEND ␈↓
␈↓ ↓H␈↓                         ␈↓↓≡ andlis[u,phi] ∧ andlis[qNIL,phi]␈↓  ...by 3.8

␈↓ ↓H␈↓Case ␈↓↓¬qn u␈↓ and ␈↓↓∀v: andlis[qd u*v,phi] ≡ andlis[qd u,phi] ∧ andlis[v,phi]␈↓

␈↓ ↓H␈↓    ␈↓↓andlis[u*v,phi] ≡ phi qa u ∧ andlis[qd u*v,phi]␈↓    ...by ␈↓¬CAR/CDR-APPEND, ␈↓␈↓¬ISTOT-APPEND, ␈↓a
␈↓ ↓H␈↓                ␈↓↓≡ phi qa u ∧ andlis[qd u,phi] ∧ andlis[v,phi]␈↓    ...by the induction hypothesis
␈↓ ↓H␈↓                ␈↓↓≡ andlis[u,phi] ∧ andlis[v,phi]␈↓    ...by 3.8.



␈↓ ↓H␈↓αProof of 3.ii .

␈↓ ↓H␈↓Method: list induction with  ␈↓↓qP[u] ≡ [andlis[u,phi] ≡ andlis[reverse u,phi]]␈↓.

␈↓ ↓H␈↓Case ␈↓↓qn u␈↓:

␈↓ ↓H␈↓    ␈↓↓andlis[reverse qNIL,phi] ≡ andlis[qNIL,phi]␈↓   ...by definition of ␈↓↓reverse␈↓

␈↓ ↓H␈↓Case ␈↓↓¬qn u␈↓ and ␈↓↓andlis[reverse qd u,phi] ≡ andlis[qd u,phi]␈↓:

␈↓ ↓H␈↓    ␈↓↓andlis[reverse u,phi] ≡ andlis[reverse qd u * <qa u>,phi]␈↓    ...by definition of ␈↓↓reverse␈↓
␈↓ ↓H␈↓                ␈↓↓≡ andlis[reverse qd u,phi] ∧ andlis[<qa u>,phi]␈↓    ...by (i)
␈↓ ↓H␈↓                        ...here we need ␈↓↓islist reverse qd u␈↓ and ␈↓↓islist <qa u>␈↓
␈↓ ↓H␈↓                ␈↓↓≡ andlis[<qa u>,phi] ∧ andlis[qd u,phi]␈↓    ...by induction hypothesis
␈↓ ↓H␈↓                ␈↓↓≡ andlis[u,phi]␈↓    ...by  3.8 and properties of <>.

␈↓ ↓H␈↓This completes Problem 3.